$\forall$$E$:Type, ${\it pred?}$:($E$$\rightarrow$($E$ + top)), $e$:$E$. first($e$) $\in$ $\mathbb{B}$